Integrating diverse formalisms into modular knowledge representation systems offers\nincreased expressivity, modeling convenience, and computational benefits. We introduce\nthe concepts of abstract inference modules and abstract modular inference systems to study\ngeneral principles behind the design and analysis of model generating programs, or solvers,\nfor integrated multi-logic systems. We show how modules and modular systems give rise\nto transition graphs, which are a natural and convenient representation of solvers, an idea\npioneered by the SAT community. These graphs lend themselves well to extensions that\ncapture such important solver design features as learning. In the paper, we consider two\nflavors of learning for modular formalisms, local and global. We illustrate our approach by\nshowing how it applies to answer set programming, propositional logic, multi-logic systems\nbased on these two formalisms and, more generally, to satisfiability modulo theories.
Loading....